(*
 * Untyped lambda calculus using De Bruijn indices.
 *)

(* Increases the depth at which nested objects are printed. *)
Control.Print.printDepth := 100;


datatype exp = var of int | lam of exp | app of exp * exp


(*
 * shift : exp -> int -> int -> exp
 * shift m l b
 * Shifts the free variables (those higher than b) in m by l.
 * This is used to avoid capturing the free variables in a substitute.
 * See the sub function below.
 *)
fun shift (var x) l b = if x > b then var (x + l) else var x
  | shift (lam m) l b = lam (shift m l (b + 1))
  | shift (app (m, n)) l b = app(shift m l b, shift n l b)

(*
 * sub : exp -> exp -> int -> int -> exp
 * sub m s x l
 * Substitutes the variable x in m by s.
 * l represents the number of binders the substitution occurs under.
 * l is used to determine how much should free variables in s be shifted by.
 *)
fun sub (var y) s x l =
      if y = x then shift s l 0     (* Variable substitution *)
      else if y > x then var (y-1)  (* Free variable *)
      else var y                    (* Bound variable *)
  | sub (lam m) s x l = lam (sub m s (x + 1) (l + 1))
  | sub (app (m, n)) s x l = app (sub m s x l, sub n s x l)

(*
 * eval : exp -> exp
 * eval m
 * Evaluates the lambda term m.
 *)
fun eval (var x) = var x
  | eval (lam m) = lam (eval m)
  | eval (app (m, n)) =
      case eval m of
        lam m' => eval (sub m' n 1 0)
      | m' => (app (m', eval n))


(* Examples *)

(*
 * Identity function
 * lambda x.x
 * lam 1
 *)
val id = lam (var 1);

(*
 * Constant function
 * lambda x.lambda y.x
 * lam lam 2
 *)
val k = lam ( lam (var 2));

eval (app (id, k));
eval (app (k, id));

(*
 * (lam lam 4 2 (lam 1 3)) (lam 5 1)
 * This should yield
 * lam 3 (lam 6 1) (lam 1 (lam 7 1))
 *)
eval (app (lam (lam (app (app (var 4, var 2), lam (app (var 1, var 3))))), lam (app (var 5, var 1))));

